FDL - Step of Proof: equal-bnot

Step of Proof: equal-bnot

Inference at *
Iof proof for Lemma equal-bnot:

x, y:

. (x = (

y))

(

(x = y))

by ((UnivCD THENA Auto)

CollapseTHEN (((AutoBoolCase y)

CollapseTHEN (((((

CRWO "eqtt_to_assert" 0)
CollapseTHENA (Auto

))

)
CCollapseTHEN (((((RWO "eqff_to_assert" 0)

CCCollapseTHENA (Auto

))

)
CCollapseTHEN (((((RW assert_pushdownC 0)
CollapseTHENA (Auto

))

)

ColCollapseTHEN (Auto

))

))

))

))

))

Co1:

Co1: 1. x :

Co1: 2. y :

Co1: 3.

(

y)
Co1: 4.

x
Co1:

(

x)
Co2:

Co2: 1. x :

Co2: 2. y :

Co2: 3.

(

y)
Co2: 4.

(

x)
Co2:

x
Co.

Definitions left + right, Unit, , tt, ff, , Type, p q, p q, p q, b, a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, x:A. B(x), t T, s = t, P Q, P & Q, x:A B(x), P Q, False, P Q, x:AB(x), Void, A, , b

Lemmas iff transitivity, btrue wf, bfalse wf, eqtt to assert, bool wf, eqff to assert, bnot wf, iff functionality wrt iff, iff wf, rev implies wf, not functionality wrt iff, assert of bnot, not wf, assert wf